M1, M2:MsgA. M1 ||decl M2  (M1  M2  MsgA) 

latex

Definitions

P  Q, x:A. B(x), x. t(x), Knd, Type, f  g, Void, KindDeq, f  g, rcv(l,tg), Top, IdLnk, t.1, Id, IdDeq, f(x)?z, type List, t  T, x.A(x), State(ds), x:AB(x), x:A  B(x), a:A fp B(a), x:A.B(x), s = t, b, f || g, <a, b>, True, T, t.2, , , Atom$n, Valtype(da;k), , P & Q, FinProbSpace, product-deq(A;B;a;b), IdLnkDeq, mk-ma, MsgA, M1  M2, M1 ||decl M2

Lemmas

msga wf, mk-ma wf, IdLnk wf, ma-valtype wf, idlnk-deq wf, product-deq wf, fpf-join wf, finite-prob-space wf, fpf-trivial-subtype-top, Id wf, id-deq wf, fpf-compatible wf, Knd wf, Kind-deq wf, squash wf, true wf, bool wf, rationals wf, pi1 wf, top wf, rcv wf, pi2 wf, fpf-sub-join-left, fpf wf, subtype-fpf2, ma-state wf, subtype rel product, subtype rel dep function, subtype rel self, subtype rel function, fpf-cap wf, subtype rel list, subtype-fpf-cap-top, subtype-fpf-cap-void, fpf-sub-join-right